es:ES, A:Type, R:(EA).
(e:E. Dec(a:A. R(e,a)))
 (X:AbsInterface(A). (e:E. (((e  X))  (a:A. R(e,a))) & (((e  X))  R(e,X(e))))) 

latex

Definitions	, Dec(P), Type, ES, P & Q, P  Q, x(s1,s2), f(a), b, E, P  Q, strong-subtype(A;B), t  T, s = t, x:A. B(x), x:AB(x), x:A. B(x), x:A  B(x), AbsInterface(A), e  X, X(e), x.A(x), case b of inl(x) => s(x) | inr(y) => t(y), inl x , t.1, inr x , , P  Q, left + right, can-apply(f;x), do-apply(f;x), True, A, P  Q, False, Top
Lemmas	false wf, true wf, es-interface wf, es-E wf, iff wf, assert wf, decidable wf, event system wf